AI 辅助理论算法发现

AI 辅助理论算法发现指把大模型的组合搜索能力放进形式化或半形式化验证框架中，让模型提出候选算法，再由可计算验证器给出 worst-case guarantee 或证明失败。它不是让 LLM 自己“相信”一个证明，而是把创造性搜索和可靠性验证拆开。

观察

LegoNE 的关键不是单纯让 LLM 写算法，而是把近似纳什均衡算法的证明问题转化成有限规模优化问题。候选算法能否成立，由优化问题给出的最坏情况 ε 保证判断。
这种范式适合理论计算机科学中的一类问题：人类能把已有证明技巧抽象成可组合模块，并设计验证器；AI 在模块空间中搜索组合，验证器负责淘汰不成立的结构。
与一般 AI for Science 相比，这里的“实验仪器”是形式化验证器或优化器。创造力来自搜索，可靠性来自验证。
对 AI 理论边界来说，这提供了一个细化判断：AI 不能越过数学证明要求，但可以在由人类定义的理论语言和证明规则中探索人类没有系统枚举过的结构。
这种路线也提醒科研工作流需要把“发现”和“证成”分离。LLM 的输出本身不是结论；只有通过可审计验证流程，才能进入理论知识。